Multi-Completion with Termination Tools
Identifieur interne : 001E16 ( Main/Exploration ); précédent : 001E15; suivant : 001E17Multi-Completion with Termination Tools
Auteurs : Sarah Winkler [Autriche] ; Haruhiko Sato [Japon] ; Aart Middeldorp [Autriche] ; Masahito Kurihara [Japon]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2013-03-01.
English descriptors
Abstract
Abstract: Knuth–Bendix completion is a classical calculus in automated deduction for transforming a set of equations into a confluent and terminating set of directed equations which can be used to decide the induced equational theory. Multi-completion with termination tools constitutes an approach that differs from the classical method in two respects: (1) external termination tools replace the reduction order—a typically critical parameter—as proposed by Wehrman et al. (2006), and (2) multi-completion as introduced by Kurihara and Kondo (1999) is used to keep track of multiple orientations in parallel while exploiting sharing to boost efficiency. In this paper we describe the inference system, give the full proof of its correctness and comment on completeness issues. Critical pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe the implementation of our approach in the tool $\mathsf{mkbTT}$ , present extensive experimental results and report on new completions.
Url:
DOI: 10.1007/s10817-012-9249-2
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000524
- to stream Istex, to step Curation: 000520
- to stream Istex, to step Checkpoint: 000405
- to stream Main, to step Merge: 001E35
- to stream Main, to step Curation: 001E16
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Multi-Completion with Termination Tools</title><author><name sortKey="Winkler, Sarah" sort="Winkler, Sarah" uniqKey="Winkler S" first="Sarah" last="Winkler">Sarah Winkler</name></author><author><name sortKey="Sato, Haruhiko" sort="Sato, Haruhiko" uniqKey="Sato H" first="Haruhiko" last="Sato">Haruhiko Sato</name></author><author><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name></author><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:177D2229F64391345DD8ABC9E9BF948984293CD6</idno><date when="2012" year="2012">2012</date><idno type="doi">10.1007/s10817-012-9249-2</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-3861GN2Z-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000524</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000524</idno><idno type="wicri:Area/Istex/Curation">000520</idno><idno type="wicri:Area/Istex/Checkpoint">000405</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000405</idno><idno type="wicri:doubleKey">0168-7433:2012:Winkler S:multi:completion:with</idno><idno type="wicri:Area/Main/Merge">001E35</idno><idno type="wicri:Area/Main/Curation">001E16</idno><idno type="wicri:Area/Main/Exploration">001E16</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Multi-Completion with Termination Tools</title><author><name sortKey="Winkler, Sarah" sort="Winkler, Sarah" uniqKey="Winkler S" first="Sarah" last="Winkler">Sarah Winkler</name><affiliation wicri:level="1"><country xml:lang="fr">Autriche</country><wicri:regionArea>Institute of Computer Science, University of Innsbruck, Innsbruck</wicri:regionArea><wicri:noRegion>Innsbruck</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Autriche</country></affiliation></author><author><name sortKey="Sato, Haruhiko" sort="Sato, Haruhiko" uniqKey="Sato H" first="Haruhiko" last="Sato">Haruhiko Sato</name><affiliation wicri:level="1"><country xml:lang="fr">Japon</country><wicri:regionArea>Graduate School of Information Science and Technology, Hokkaido University, Hokkaido</wicri:regionArea><wicri:noRegion>Hokkaido</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Japon</country></affiliation></author><author><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name><affiliation wicri:level="1"><country xml:lang="fr">Autriche</country><wicri:regionArea>Institute of Computer Science, University of Innsbruck, Innsbruck</wicri:regionArea><wicri:noRegion>Innsbruck</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Autriche</country></affiliation></author><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><affiliation wicri:level="1"><country xml:lang="fr">Japon</country><wicri:regionArea>Graduate School of Information Science and Technology, Hokkaido University, Hokkaido</wicri:regionArea><wicri:noRegion>Hokkaido</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Japon</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2013-03-01">2013-03-01</date><biblScope unit="volume">50</biblScope><biblScope unit="issue">3</biblScope><biblScope unit="page" from="317">317</biblScope><biblScope unit="page" to="354">354</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Knuth–Bendix completion</term><term>Multi-completion</term><term>Term rewriting</term><term>Termination tools</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Knuth–Bendix completion is a classical calculus in automated deduction for transforming a set of equations into a confluent and terminating set of directed equations which can be used to decide the induced equational theory. Multi-completion with termination tools constitutes an approach that differs from the classical method in two respects: (1) external termination tools replace the reduction order—a typically critical parameter—as proposed by Wehrman et al. (2006), and (2) multi-completion as introduced by Kurihara and Kondo (1999) is used to keep track of multiple orientations in parallel while exploiting sharing to boost efficiency. In this paper we describe the inference system, give the full proof of its correctness and comment on completeness issues. Critical pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe the implementation of our approach in the tool $\mathsf{mkbTT}$ , present extensive experimental results and report on new completions.</div></front></TEI><affiliations><list><country><li>Autriche</li><li>Japon</li></country></list><tree><country name="Autriche"><noRegion><name sortKey="Winkler, Sarah" sort="Winkler, Sarah" uniqKey="Winkler S" first="Sarah" last="Winkler">Sarah Winkler</name></noRegion><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name><name sortKey="Winkler, Sarah" sort="Winkler, Sarah" uniqKey="Winkler S" first="Sarah" last="Winkler">Sarah Winkler</name></country><country name="Japon"><noRegion><name sortKey="Sato, Haruhiko" sort="Sato, Haruhiko" uniqKey="Sato H" first="Haruhiko" last="Sato">Haruhiko Sato</name></noRegion><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><name sortKey="Sato, Haruhiko" sort="Sato, Haruhiko" uniqKey="Sato H" first="Haruhiko" last="Sato">Haruhiko Sato</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001E16 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001E16 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:177D2229F64391345DD8ABC9E9BF948984293CD6
|texte= Multi-Completion with Termination Tools
}}
| This area was generated with Dilib version V0.6.33. |  |